We present for the first time an exhaustive enumeration of Williamson matrices of even order n < 65. The search method relies on the novel SAT+CAS paradigm of coupling SAT solvers with computer algebra systems so as to take advantage of the advances made in both the field of satisfiability checking and the field of symbolic computation. Additionally, we use a programmatic SAT solver which allows conflict clauses to be learned programmatically, through a piece of code specifically tailored to the domain area. Prior to our work, Williamson matrices had only been enumerated for odd orders n < 60, so our work increases the bounds that Williamson matrices have been enumerated up to and provides the first enumeration of Williamson matrices of even order. Our results show that Williamson matrices of even order tend to be much more abundant than those of odd orders. In particular, Williamson matrices exist for every even order n < 65 but do not exist in orders 35, 47, 53, and 59.

A computer algebra system (CAS) is a software program that allows computation over mathematical expressions in a way which is similar to the traditional manual computations of mathematicians and scientists. The development of the computer algebra systems in the second half of the 20th century is part of the discipline of "computer algebra" or "symbolic computation", which has spurred work in algorithms over mathematical objects such as polynomials. Computer algebra systems may be divided in two classes: the specialized ones and the general purpose ones. The specialized ones are devoted to a specific part of mathematics, such as number theory, group theory, or teaching of elementary mathematics. General purpose computer algebra systems aim to be useful to a user working in any scientific field that requires manipulation of mathematical expressions. The library must cover not only the needs of the users, but also the needs of the simplifier.